Music

Music

So today we start entirely new

Music

So linear logic is our

Linear logic is our new

Is the new formalism that we want to attack

And actually both linear logic and the logic of band implications

That we want to attack next can be seen as falling into broader

Umbrellab substructural logic

So maybe before I tell you more about specifically

Linear logic itself, especially that involves lots of connectives

And it would be rather strange to throw all of this together

Maybe let's go slowly and see where the idea could possibly come from

And why linear logic is such a crazy interesting

And actually much easier to understand than it may seem at the beginning

So maybe let's state a few things at the very beginning

So the Grenzel calculi that we were using so far

For both intuitionistic logic and classical logic

They were carefully designed to fulfill several purposes

And also in the model case

For example we wanted to be able to, as I already told you

One of the goals was that by failing proof-self

We wanted to be able to immediately accept counter models

And they were built in such a way that structural rules

Such as weakening and contraction

They were derived rather than assumed

And this is fine but this is not the only way

In which one could possibly do Grenzel calculi for intuitionistic

Or for classical logic or another system

And we may wonder then what would happen if we don't assume

That we have such structural rules

When those rules are added on top rather than against a system

Which allows us a little bit more freedom to decide

So first of all we have several ways in which we could approach

Connectives like conjunction and disjunction even

And basic ways how you combine information

On the left and on the right hand side of the sequence

So should I write anything for what I said?

Probably not

Okay so let's just state that in absence of structural rules

Especially weakening and contraction

Traditionally one also includes exchange among structural rules

Exchange is simply the idea that you can write premises in any order

On the left hand side of the ten style or ten style sequinaro

Or also whatever you write on the right hand side of the sequinaro

But here it is kind of built in

Because we assume that we are dealing with multisets all the time

If we wanted to be even more careful then we would start with lists

Then we would have explicitly to say if we allow